(declare-fun _substvar_908_ () Real)
(declare-fun _substvar_1085_ () Bool)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(assert (or (< r4 r1 (* r4 r4 r5) r3) _substvar_1085_))
(assert (>= _substvar_908_ r1 r1 838.7))
(check-sat)
